(0) Obligation:

Clauses:

even(0, true).
even(s(0), false).
even(s(s(X)), B) :- even(X, B).
half(0, 0).
half(s(s(X)), s(Y)) :- half(X, Y).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(even(s(X), B), if(B, s(X), Y, Z)).
if(true, s(X), Y, Z) :- ','(half(s(X), X1), ','(times(X1, Y, Y1), plus(Y1, Y1, Z))).
if(false, s(X), Y, Z) :- ','(times(X, Y, U), plus(Y, U, Z)).

Query: times(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

plusA(s(X1), X2, s(X3)) :- plusA(X1, X2, X3).
evenB(s(s(X1)), X2) :- evenB(X1, X2).
halfC(s(s(X1)), s(X2)) :- halfC(X1, X2).
timesD(s(X1), X2, X3) :- evenB(s(X1), X4).
timesD(s(X1), X2, X3) :- ','(evencB(s(X1), true), halfC(s(X1), X4)).
timesD(s(X1), X2, X3) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X4), timesD(X4, X2, X5))).
timesD(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X4), ','(timescD(X4, X2, s(s(s(s(s(s(s(s(X5))))))))), plusE(X5, s(s(s(s(s(s(s(X5))))))), X3)))).
timesD(s(X1), X2, X3) :- ','(evencB(s(X1), false), timesD(X1, X2, X4)).
timesD(s(X1), X2, X3) :- ','(evencB(s(X1), false), ','(timescD(X1, X2, X4), plusF(X2, X4, X3))).
plusE(s(X1), X2, s(X3)) :- plusE(X1, X2, X3).
plusF(s(X1), X2, s(X3)) :- plusF(X1, X2, X3).
timesI(s(0), X1, X2) :- ','(timescG(X1, X3), plusA(X1, X3, X2)).
timesI(s(s(X1)), X2, X3) :- evenB(X1, X4).
timesI(s(s(X1)), X2, X3) :- ','(evencB(X1, true), halfC(X1, X4)).
timesI(s(s(X1)), X2, X3) :- ','(evencB(X1, true), ','(halfcH(X1, X4), timesD(X4, X2, X5))).
timesI(s(s(X1)), X2, s(s(s(s(s(s(s(s(X3))))))))) :- ','(evencB(X1, true), ','(halfcH(X1, X4), ','(timescD(X4, X2, s(s(s(s(s(s(s(s(X5))))))))), plusA(X5, s(s(s(s(s(s(s(s(X5)))))))), X3)))).
timesI(s(s(X1)), X2, X3) :- ','(evencB(X1, false), timesD(s(X1), X2, X4)).
timesI(s(s(X1)), X2, X3) :- ','(evencB(X1, false), ','(timescD(s(X1), X2, X4), plusA(X2, X4, X3))).

Clauses:

pluscA(0, X1, X1).
pluscA(s(X1), X2, s(X3)) :- pluscA(X1, X2, X3).
evencB(0, true).
evencB(s(0), false).
evencB(s(s(X1)), X2) :- evencB(X1, X2).
halfcC(0, 0).
halfcC(s(s(X1)), s(X2)) :- halfcC(X1, X2).
timescD(0, X1, 0).
timescD(s(X1), X2, 0) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, 0))).
timescD(s(X1), X2, s(s(0))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(0)))).
timescD(s(X1), X2, s(s(s(s(0))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(s(0))))).
timescD(s(X1), X2, s(s(s(s(s(s(0))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(s(s(0)))))).
timescD(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(s(s(s(0))))))).
timescD(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(s(s(s(s(0)))))))).
timescD(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(s(s(s(s(s(0))))))))).
timescD(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X3), timescD(X3, X2, s(s(s(s(s(s(s(0)))))))))).
timescD(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) :- ','(evencB(s(X1), true), ','(halfcC(s(X1), X4), ','(timescD(X4, X2, s(s(s(s(s(s(s(s(X5))))))))), pluscE(X5, s(s(s(s(s(s(s(X5))))))), X3)))).
timescD(s(X1), X2, X3) :- ','(evencB(s(X1), false), ','(timescD(X1, X2, X4), pluscF(X2, X4, X3))).
pluscE(0, X1, s(X1)).
pluscE(s(X1), X2, s(X3)) :- pluscE(X1, X2, X3).
pluscF(0, X1, X1).
pluscF(s(X1), X2, s(X3)) :- pluscF(X1, X2, X3).
timescG(X1, 0).
halfcH(X1, s(X2)) :- halfcC(X1, X2).

Afs:

timesI(x1, x2, x3)  =  timesI(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
timesI_in: (b,b,f)
plusA_in: (b,b,f)
evenB_in: (b,f)
evencB_in: (b,b)
halfC_in: (b,f)
halfcH_in: (b,f)
halfcC_in: (b,f)
timesD_in: (b,b,f)
timescD_in: (b,b,f) (b,b,b)
pluscF_in: (b,b,f) (b,b,b)
pluscE_in: (b,b,f) (b,b,b)
plusE_in: (b,b,f)
plusF_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TIMESI_IN_GGA(s(0), X1, X2) → U19_GGA(X1, X2, timescG_in_ga(X1, X3))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → U20_GGA(X1, X2, plusA_in_gga(X1, X3, X2))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → PLUSA_IN_GGA(X1, X3, X2)
PLUSA_IN_GGA(s(X1), X2, s(X3)) → U1_GGA(X1, X2, X3, plusA_in_gga(X1, X2, X3))
PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U21_GGA(X1, X2, X3, evenB_in_ga(X1, X4))
TIMESI_IN_GGA(s(s(X1)), X2, X3) → EVENB_IN_GA(X1, X4)
EVENB_IN_GA(s(s(X1)), X2) → U2_GA(X1, X2, evenB_in_ga(X1, X2))
EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U22_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U23_GGA(X1, X2, X3, halfC_in_ga(X1, X4))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → HALFC_IN_GA(X1, X4)
HALFC_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfC_in_ga(X1, X2))
HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U24_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U25_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U4_GGA(X1, X2, X3, evenB_in_ga(s(X1), X4))
TIMESD_IN_GGA(s(X1), X2, X3) → EVENB_IN_GA(s(X1), X4)
TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U6_GGA(X1, X2, X3, halfC_in_ga(s(X1), X4))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → HALFC_IN_GA(s(X1), X4)
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U8_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U9_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U9_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U10_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U10_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U11_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U12_GGA(X1, X2, X3, plusE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSE_IN_GGA(X5, s(s(s(s(s(s(s(X5))))))), X3)
PLUSE_IN_GGA(s(X1), X2, s(X3)) → U17_GGA(X1, X2, X3, plusE_in_gga(X1, X2, X3))
PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U14_GGA(X1, X2, X3, timesD_in_gga(X1, X2, X4))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U15_GGA(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U16_GGA(X1, X2, X3, plusF_in_gga(X2, X4, X3))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → PLUSF_IN_GGA(X2, X4, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → U18_GGA(X1, X2, X3, plusF_in_gga(X1, X2, X3))
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, s(s(s(s(s(s(s(s(X3))))))))) → U26_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U26_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U27_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U27_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U28_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U29_GGA(X1, X2, X3, plusA_in_gga(X5, s(s(s(s(s(s(s(s(X5)))))))), X3))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSA_IN_GGA(X5, s(s(s(s(s(s(s(s(X5)))))))), X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U30_GGA(X1, X2, X3, evencB_in_gg(X1, false))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U31_GGA(X1, X2, X3, timesD_in_gga(s(X1), X2, X4))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → TIMESD_IN_GGA(s(X1), X2, X4)
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U32_GGA(X1, X2, X3, timescD_in_gga(s(X1), X2, X4))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → U33_GGA(X1, X2, X3, plusA_in_gga(X2, X4, X3))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → PLUSA_IN_GGA(X2, X4, X3)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
plusA_in_gga(x1, x2, x3)  =  plusA_in_gga(x1, x2)
evenB_in_ga(x1, x2)  =  evenB_in_ga(x1)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timesD_in_gga(x1, x2, x3)  =  timesD_in_gga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusE_in_gga(x1, x2, x3)  =  plusE_in_gga(x1, x2)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
TIMESI_IN_GGA(x1, x2, x3)  =  TIMESI_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
U20_GGA(x1, x2, x3)  =  U20_GGA(x1, x3)
PLUSA_IN_GGA(x1, x2, x3)  =  PLUSA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x1, x2, x4)
EVENB_IN_GA(x1, x2)  =  EVENB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
TIMESD_IN_GGA(x1, x2, x3)  =  TIMESD_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
PLUSE_IN_GGA(x1, x2, x3)  =  PLUSE_IN_GGA(x1, x2)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4)  =  U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4)  =  U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4)  =  U33_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESI_IN_GGA(s(0), X1, X2) → U19_GGA(X1, X2, timescG_in_ga(X1, X3))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → U20_GGA(X1, X2, plusA_in_gga(X1, X3, X2))
U19_GGA(X1, X2, timescG_out_ga(X1, X3)) → PLUSA_IN_GGA(X1, X3, X2)
PLUSA_IN_GGA(s(X1), X2, s(X3)) → U1_GGA(X1, X2, X3, plusA_in_gga(X1, X2, X3))
PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U21_GGA(X1, X2, X3, evenB_in_ga(X1, X4))
TIMESI_IN_GGA(s(s(X1)), X2, X3) → EVENB_IN_GA(X1, X4)
EVENB_IN_GA(s(s(X1)), X2) → U2_GA(X1, X2, evenB_in_ga(X1, X2))
EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U22_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U23_GGA(X1, X2, X3, halfC_in_ga(X1, X4))
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → HALFC_IN_GA(X1, X4)
HALFC_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfC_in_ga(X1, X2))
HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)
U22_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U24_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U25_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U24_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U4_GGA(X1, X2, X3, evenB_in_ga(s(X1), X4))
TIMESD_IN_GGA(s(X1), X2, X3) → EVENB_IN_GA(s(X1), X4)
TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U6_GGA(X1, X2, X3, halfC_in_ga(s(X1), X4))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → HALFC_IN_GA(s(X1), X4)
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U8_GGA(X1, X2, X3, timesD_in_gga(X4, X2, X5))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U9_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U9_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U10_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U10_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U11_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U12_GGA(X1, X2, X3, plusE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
U11_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSE_IN_GGA(X5, s(s(s(s(s(s(s(X5))))))), X3)
PLUSE_IN_GGA(s(X1), X2, s(X3)) → U17_GGA(X1, X2, X3, plusE_in_gga(X1, X2, X3))
PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U14_GGA(X1, X2, X3, timesD_in_gga(X1, X2, X4))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → U15_GGA(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U16_GGA(X1, X2, X3, plusF_in_gga(X2, X4, X3))
U15_GGA(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → PLUSF_IN_GGA(X2, X4, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → U18_GGA(X1, X2, X3, plusF_in_gga(X1, X2, X3))
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
TIMESI_IN_GGA(s(s(X1)), X2, s(s(s(s(s(s(s(s(X3))))))))) → U26_GGA(X1, X2, X3, evencB_in_gg(X1, true))
U26_GGA(X1, X2, X3, evencB_out_gg(X1, true)) → U27_GGA(X1, X2, X3, halfcH_in_ga(X1, X4))
U27_GGA(X1, X2, X3, halfcH_out_ga(X1, X4)) → U28_GGA(X1, X2, X3, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U29_GGA(X1, X2, X3, plusA_in_gga(X5, s(s(s(s(s(s(s(s(X5)))))))), X3))
U28_GGA(X1, X2, X3, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → PLUSA_IN_GGA(X5, s(s(s(s(s(s(s(s(X5)))))))), X3)
TIMESI_IN_GGA(s(s(X1)), X2, X3) → U30_GGA(X1, X2, X3, evencB_in_gg(X1, false))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U31_GGA(X1, X2, X3, timesD_in_gga(s(X1), X2, X4))
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → TIMESD_IN_GGA(s(X1), X2, X4)
U30_GGA(X1, X2, X3, evencB_out_gg(X1, false)) → U32_GGA(X1, X2, X3, timescD_in_gga(s(X1), X2, X4))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → U33_GGA(X1, X2, X3, plusA_in_gga(X2, X4, X3))
U32_GGA(X1, X2, X3, timescD_out_gga(s(X1), X2, X4)) → PLUSA_IN_GGA(X2, X4, X3)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
plusA_in_gga(x1, x2, x3)  =  plusA_in_gga(x1, x2)
evenB_in_ga(x1, x2)  =  evenB_in_ga(x1)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timesD_in_gga(x1, x2, x3)  =  timesD_in_gga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusE_in_gga(x1, x2, x3)  =  plusE_in_gga(x1, x2)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
TIMESI_IN_GGA(x1, x2, x3)  =  TIMESI_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
U20_GGA(x1, x2, x3)  =  U20_GGA(x1, x3)
PLUSA_IN_GGA(x1, x2, x3)  =  PLUSA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x1, x2, x4)
EVENB_IN_GA(x1, x2)  =  EVENB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
TIMESD_IN_GGA(x1, x2, x3)  =  TIMESD_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
PLUSE_IN_GGA(x1, x2, x3)  =  PLUSE_IN_GGA(x1, x2)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4)  =  U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4)  =  U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4)  =  U33_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 41 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUSF_IN_GGA(s(X1), X2) → PLUSF_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUSF_IN_GGA(s(X1), X2) → PLUSF_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
PLUSE_IN_GGA(x1, x2, x3)  =  PLUSE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSE_IN_GGA(s(X1), X2, s(X3)) → PLUSE_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSE_IN_GGA(x1, x2, x3)  =  PLUSE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUSE_IN_GGA(s(X1), X2) → PLUSE_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUSE_IN_GGA(s(X1), X2) → PLUSE_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALFC_IN_GA(s(s(X1)), s(X2)) → HALFC_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HALFC_IN_GA(s(s(X1))) → HALFC_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • HALFC_IN_GA(s(s(X1))) → HALFC_IN_GA(X1)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
EVENB_IN_GA(x1, x2)  =  EVENB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

EVENB_IN_GA(s(s(X1)), X2) → EVENB_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
EVENB_IN_GA(x1, x2)  =  EVENB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EVENB_IN_GA(s(s(X1))) → EVENB_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • EVENB_IN_GA(s(s(X1))) → EVENB_IN_GA(X1)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
TIMESD_IN_GGA(x1, x2, x3)  =  TIMESD_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESD_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, X3, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U7_GGA(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2, X5)
TIMESD_IN_GGA(s(X1), X2, X3) → U13_GGA(X1, X2, X3, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, X3, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2, X4)

The TRS R consists of the following rules:

evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
TIMESD_IN_GGA(x1, x2, x3)  =  TIMESD_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U13_GGA(X1, X2, evencB_in_gg(s(X1), false))
U13_GGA(X1, X2, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2)

The TRS R consists of the following rules:

evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)

The set Q consists of the following terms:

evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


TIMESD_IN_GGA(s(X1), X2) → U13_GGA(X1, X2, evencB_in_gg(s(X1), false))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(TIMESD_IN_GGA(x1, x2)) = x1   
POL(U13_GGA(x1, x2, x3)) = x1   
POL(U36_gg(x1, x2, x3)) = 0   
POL(U37_ga(x1, x2)) = 1 + x2   
POL(U5_GGA(x1, x2, x3)) = 1 + x1   
POL(U7_GGA(x1, x2, x3)) = x3   
POL(evencB_in_gg(x1, x2)) = 0   
POL(evencB_out_gg(x1, x2)) = 0   
POL(false) = 0   
POL(halfcC_in_ga(x1)) = x1   
POL(halfcC_out_ga(x1, x2)) = x2   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
halfcC_in_ga(0) → halfcC_out_ga(0, 0)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))
U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
U13_GGA(X1, X2, evencB_out_gg(s(X1), false)) → TIMESD_IN_GGA(X1, X2)

The TRS R consists of the following rules:

evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)

The set Q consists of the following terms:

evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(42) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))

The TRS R consists of the following rules:

evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)

The set Q consists of the following terms:

evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(44) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(TIMESD_IN_GGA(x1, x2)) = 0   
POL(U36_gg(x1, x2, x3)) = x3   
POL(U37_ga(x1, x2)) = 0   
POL(U5_GGA(x1, x2, x3)) = 2·x3   
POL(U7_GGA(x1, x2, x3)) = 0   
POL(evencB_in_gg(x1, x2)) = x2   
POL(evencB_out_gg(x1, x2)) = 0   
POL(false) = 2   
POL(halfcC_in_ga(x1)) = 0   
POL(halfcC_out_ga(x1, x2)) = 0   
POL(s(x1)) = 0   
POL(true) = 0   

(45) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))

The TRS R consists of the following rules:

evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)

The set Q consists of the following terms:

evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(46) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

halfcC_in_ga(s(s(X1))) → U37_ga(X1, halfcC_in_ga(X1))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(TIMESD_IN_GGA(x1, x2)) = 2·x1   
POL(U36_gg(x1, x2, x3)) = x2   
POL(U37_ga(x1, x2)) = 2 + x2   
POL(U5_GGA(x1, x2, x3)) = 2·x1 + 2·x3   
POL(U7_GGA(x1, x2, x3)) = 2·x3   
POL(evencB_in_gg(x1, x2)) = x2   
POL(evencB_out_gg(x1, x2)) = x2   
POL(halfcC_in_ga(x1)) = x1   
POL(halfcC_out_ga(x1, x2)) = x2   
POL(s(x1)) = 2 + x1   
POL(true) = 2   

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_GGA(X1, X2, evencB_out_gg(s(X1), true)) → U7_GGA(X1, X2, halfcC_in_ga(s(X1)))
U7_GGA(X1, X2, halfcC_out_ga(s(X1), X4)) → TIMESD_IN_GGA(X4, X2)
TIMESD_IN_GGA(s(X1), X2) → U5_GGA(X1, X2, evencB_in_gg(s(X1), true))

The TRS R consists of the following rules:

evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
U37_ga(X1, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
evencB_in_gg(0, true) → evencB_out_gg(0, true)
halfcC_in_ga(0) → halfcC_out_ga(0, 0)

The set Q consists of the following terms:

evencB_in_gg(x0, x1)
halfcC_in_ga(x0)
U36_gg(x0, x1, x2)
U37_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(48) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(49) TRUE

(50) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

timescG_in_ga(X1, 0) → timescG_out_ga(X1, 0)
evencB_in_gg(0, true) → evencB_out_gg(0, true)
evencB_in_gg(s(0), false) → evencB_out_gg(s(0), false)
evencB_in_gg(s(s(X1)), X2) → U36_gg(X1, X2, evencB_in_gg(X1, X2))
U36_gg(X1, X2, evencB_out_gg(X1, X2)) → evencB_out_gg(s(s(X1)), X2)
halfcH_in_ga(X1, s(X2)) → U71_ga(X1, X2, halfcC_in_ga(X1, X2))
halfcC_in_ga(0, 0) → halfcC_out_ga(0, 0)
halfcC_in_ga(s(s(X1)), s(X2)) → U37_ga(X1, X2, halfcC_in_ga(X1, X2))
U37_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcC_out_ga(s(s(X1)), s(X2))
U71_ga(X1, X2, halfcC_out_ga(X1, X2)) → halfcH_out_ga(X1, s(X2))
timescD_in_gga(0, X1, 0) → timescD_out_gga(0, X1, 0)
timescD_in_gga(s(X1), X2, 0) → U38_gga(X1, X2, evencB_in_gg(s(X1), true))
U38_gga(X1, X2, evencB_out_gg(s(X1), true)) → U39_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U39_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_gga(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(0, X1, 0) → timescD_out_ggg(0, X1, 0)
timescD_in_ggg(s(X1), X2, 0) → U38_ggg(X1, X2, evencB_in_gg(s(X1), true))
U38_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U39_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U39_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U40_ggg(X1, X2, timescD_in_ggg(X3, X2, 0))
timescD_in_ggg(s(X1), X2, s(s(0))) → U41_ggg(X1, X2, evencB_in_gg(s(X1), true))
U41_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U42_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U42_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_ggg(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, s(s(s(s(0))))) → U44_ggg(X1, X2, evencB_in_gg(s(X1), true))
U44_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U45_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U45_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_ggg(X1, X2, evencB_in_gg(s(X1), true))
U47_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U48_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U48_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_ggg(X1, X2, evencB_in_gg(s(X1), true))
U50_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U51_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U51_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_ggg(X1, X2, evencB_in_gg(s(X1), true))
U53_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U54_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U54_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_ggg(X1, X2, evencB_in_gg(s(X1), true))
U56_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U57_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U57_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_ggg(X1, X2, evencB_in_gg(s(X1), true))
U59_ggg(X1, X2, evencB_out_gg(s(X1), true)) → U60_ggg(X1, X2, halfcC_in_ga(s(X1), X3))
U60_ggg(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_ggg(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
timescD_in_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_ggg(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_ggg(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_ggg(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_ggg(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_ggg(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, s(s(0))) → U41_gga(X1, X2, evencB_in_gg(s(X1), true))
U41_gga(X1, X2, evencB_out_gg(s(X1), true)) → U42_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U42_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U43_gga(X1, X2, timescD_in_ggg(X3, X2, s(0)))
timescD_in_ggg(s(X1), X2, X3) → U66_ggg(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_ggg(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_ggg(X1, X2, X3, timescD_in_gga(X1, X2, X4))
timescD_in_gga(s(X1), X2, s(s(s(s(0))))) → U44_gga(X1, X2, evencB_in_gg(s(X1), true))
U44_gga(X1, X2, evencB_out_gg(s(X1), true)) → U45_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U45_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U46_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(0))))
U46_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_gga(s(X1), X2, s(s(s(s(0)))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(0))))))) → U47_gga(X1, X2, evencB_in_gg(s(X1), true))
U47_gga(X1, X2, evencB_out_gg(s(X1), true)) → U48_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U48_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U49_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(0)))))
U49_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(0)))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(0))))))))) → U50_gga(X1, X2, evencB_in_gg(s(X1), true))
U50_gga(X1, X2, evencB_out_gg(s(X1), true)) → U51_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U51_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U52_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(0))))))
U52_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U53_gga(X1, X2, evencB_in_gg(s(X1), true))
U53_gga(X1, X2, evencB_out_gg(s(X1), true)) → U54_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U54_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U55_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(0)))))))
U55_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U56_gga(X1, X2, evencB_in_gg(s(X1), true))
U56_gga(X1, X2, evencB_out_gg(s(X1), true)) → U57_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U57_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U58_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(0))))))))
U58_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U59_gga(X1, X2, evencB_in_gg(s(X1), true))
U59_gga(X1, X2, evencB_out_gg(s(X1), true)) → U60_gga(X1, X2, halfcC_in_ga(s(X1), X3))
U60_gga(X1, X2, halfcC_out_ga(s(X1), X3)) → U61_gga(X1, X2, timescD_in_ggg(X3, X2, s(s(s(s(s(s(s(0)))))))))
U61_gga(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timescD_in_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3))))))))) → U62_gga(X1, X2, X3, evencB_in_gg(s(X1), true))
U62_gga(X1, X2, X3, evencB_out_gg(s(X1), true)) → U63_gga(X1, X2, X3, halfcC_in_ga(s(X1), X4))
U63_gga(X1, X2, X3, halfcC_out_ga(s(X1), X4)) → U64_gga(X1, X2, X3, X4, timescD_in_gga(X4, X2, s(s(s(s(s(s(s(s(X5))))))))))
timescD_in_gga(s(X1), X2, X3) → U66_gga(X1, X2, X3, evencB_in_gg(s(X1), false))
U66_gga(X1, X2, X3, evencB_out_gg(s(X1), false)) → U67_gga(X1, X2, X3, timescD_in_gga(X1, X2, X4))
U67_gga(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U70_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U70_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U68_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescD_out_gga(s(X1), X2, X3)
U64_gga(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_gga(X1, X2, X3, pluscE_in_gga(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_gga(0, X1, s(X1)) → pluscE_out_gga(0, X1, s(X1))
pluscE_in_gga(s(X1), X2, s(X3)) → U69_gga(X1, X2, X3, pluscE_in_gga(X1, X2, X3))
U69_gga(X1, X2, X3, pluscE_out_gga(X1, X2, X3)) → pluscE_out_gga(s(X1), X2, s(X3))
U65_gga(X1, X2, X3, pluscE_out_gga(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_gga(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U67_ggg(X1, X2, X3, timescD_out_gga(X1, X2, X4)) → U68_ggg(X1, X2, X3, pluscF_in_ggg(X2, X4, X3))
pluscF_in_ggg(0, X1, X1) → pluscF_out_ggg(0, X1, X1)
pluscF_in_ggg(s(X1), X2, s(X3)) → U70_ggg(X1, X2, X3, pluscF_in_ggg(X1, X2, X3))
U70_ggg(X1, X2, X3, pluscF_out_ggg(X1, X2, X3)) → pluscF_out_ggg(s(X1), X2, s(X3))
U68_ggg(X1, X2, X3, pluscF_out_ggg(X2, X4, X3)) → timescD_out_ggg(s(X1), X2, X3)
U43_gga(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_gga(s(X1), X2, s(s(0)))
U64_ggg(X1, X2, X3, X4, timescD_out_gga(X4, X2, s(s(s(s(s(s(s(s(X5)))))))))) → U65_ggg(X1, X2, X3, pluscE_in_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3))
pluscE_in_ggg(0, X1, s(X1)) → pluscE_out_ggg(0, X1, s(X1))
pluscE_in_ggg(s(X1), X2, s(X3)) → U69_ggg(X1, X2, X3, pluscE_in_ggg(X1, X2, X3))
U69_ggg(X1, X2, X3, pluscE_out_ggg(X1, X2, X3)) → pluscE_out_ggg(s(X1), X2, s(X3))
U65_ggg(X1, X2, X3, pluscE_out_ggg(X5, s(s(s(s(s(s(s(X5))))))), X3)) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(X3)))))))))
U61_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(s(0))))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U58_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(s(0)))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U55_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(s(0))))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U52_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(s(0)))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(s(s(0)))))))))
U49_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(s(0))))) → timescD_out_ggg(s(X1), X2, s(s(s(s(s(s(0)))))))
U46_ggg(X1, X2, timescD_out_ggg(X3, X2, s(s(0)))) → timescD_out_ggg(s(X1), X2, s(s(s(s(0)))))
U43_ggg(X1, X2, timescD_out_ggg(X3, X2, s(0))) → timescD_out_ggg(s(X1), X2, s(s(0)))
U40_ggg(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_ggg(s(X1), X2, 0)
U40_gga(X1, X2, timescD_out_ggg(X3, X2, 0)) → timescD_out_gga(s(X1), X2, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timescG_in_ga(x1, x2)  =  timescG_in_ga(x1)
timescG_out_ga(x1, x2)  =  timescG_out_ga(x1, x2)
evencB_in_gg(x1, x2)  =  evencB_in_gg(x1, x2)
true  =  true
evencB_out_gg(x1, x2)  =  evencB_out_gg(x1, x2)
false  =  false
U36_gg(x1, x2, x3)  =  U36_gg(x1, x2, x3)
halfcH_in_ga(x1, x2)  =  halfcH_in_ga(x1)
U71_ga(x1, x2, x3)  =  U71_ga(x1, x3)
halfcC_in_ga(x1, x2)  =  halfcC_in_ga(x1)
halfcC_out_ga(x1, x2)  =  halfcC_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
halfcH_out_ga(x1, x2)  =  halfcH_out_ga(x1, x2)
timescD_in_gga(x1, x2, x3)  =  timescD_in_gga(x1, x2)
timescD_out_gga(x1, x2, x3)  =  timescD_out_gga(x1, x2, x3)
U38_gga(x1, x2, x3)  =  U38_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
timescD_in_ggg(x1, x2, x3)  =  timescD_in_ggg(x1, x2, x3)
timescD_out_ggg(x1, x2, x3)  =  timescD_out_ggg(x1, x2, x3)
U38_ggg(x1, x2, x3)  =  U38_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3, x4)  =  U62_ggg(x1, x2, x3, x4)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4, x5)  =  U64_ggg(x1, x2, x3, x5)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3, x4)  =  U62_gga(x1, x2, x4)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4, x5)  =  U64_gga(x1, x2, x5)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
pluscF_in_gga(x1, x2, x3)  =  pluscF_in_gga(x1, x2)
pluscF_out_gga(x1, x2, x3)  =  pluscF_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x1, x2, x4)
pluscE_in_gga(x1, x2, x3)  =  pluscE_in_gga(x1, x2)
pluscE_out_gga(x1, x2, x3)  =  pluscE_out_gga(x1, x2, x3)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
pluscF_in_ggg(x1, x2, x3)  =  pluscF_in_ggg(x1, x2, x3)
pluscF_out_ggg(x1, x2, x3)  =  pluscF_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x1, x2, x3, x4)
pluscE_in_ggg(x1, x2, x3)  =  pluscE_in_ggg(x1, x2, x3)
pluscE_out_ggg(x1, x2, x3)  =  pluscE_out_ggg(x1, x2, x3)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
PLUSA_IN_GGA(x1, x2, x3)  =  PLUSA_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(51) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(52) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PLUSA_IN_GGA(s(X1), X2, s(X3)) → PLUSA_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSA_IN_GGA(x1, x2, x3)  =  PLUSA_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(53) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUSA_IN_GGA(s(X1), X2) → PLUSA_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(55) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUSA_IN_GGA(s(X1), X2) → PLUSA_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

(56) YES